<!DOCTYPE html>
<html lang="en" dir="ltr" class="no-js">
<head>
    <meta charset="utf-8" />
    <title>Workcraft - tutorial:stg:buck:start</title>
    <script>(function(H){H.className=H.className.replace(/\bno-js\b/,'js')})(document.documentElement)</script>
    <meta name="generator" content="DokuWiki"/>
<meta name="robots" content="noindex,nofollow"/>
<meta name="keywords" content="tutorial,stg,buck,start"/>
<link rel="search" type="application/opensearchdescription+xml" href="../../lib/exe/opensearch.html" title="Workcraft"/>
<link rel="start" href="start.html"/>
<link rel="contents" href="start.html" title="Sitemap"/>
<link rel="alternate" type="application/rss+xml" title="Changes" />
<link rel="alternate" type="application/rss+xml" title="Current namespace" />
<link rel="alternate" type="text/html" title="Plain HTML" href="../../_export/xhtml/tutorial/stg/buck/start.xhtml"/>
<link rel="alternate" type="text/plain" title="Wiki Markup" href="../../_export/raw/tutorial/stg/buck/start.raw"/>
<link rel="canonical" href="http://www.workcraft.org/tutorial/stg/buck/start"/>
<link rel="stylesheet" type="text/css" href="../../lib/exe/css.php.t.dokuwiki-light-export.css"/>
<script type="text/javascript">/*<![CDATA[*/var NS='tutorial:stg:buck';var JSINFO = {"id":"tutorial:stg:buck:start","namespace":"tutorial:stg:buck"};
/*!]]>*/</script>
<script type="text/javascript" charset="utf-8" src="../../lib/exe/js.php.t.dokuwiki-light-export.js"></script>
    <meta name="viewport" content="width=device-width,initial-scale=1" />
    <link rel="shortcut icon" href="../../favicon.ico" />
<link rel="apple-touch-icon" href="../../apple-touch-icon.png" />
    </head>

<body>
    <!--[if lte IE 7 ]><div id="IE7"><![endif]--><!--[if IE 8 ]><div id="IE8"><![endif]-->
    <div id="dokuwiki__site"><div id="dokuwiki__top" class="site dokuwiki mode_show tpl_dokuwiki-light-export     ">

        
<!-- ********** HEADER ********** -->
<div id="dokuwiki__header"><div class="pad group">

        <h1><a href="../../start.html"  title="Workcraft start page"><img src="../../logo.png" width="327" height="57" alt="" /></a></h1>
    
    <div class="tools group">
        <!-- USER TOOLS -->
                    <div id="dokuwiki__usertools">
                <h3 class="a11y">User Tools</h3>
                <ul>
                    <li><a href="start.html"  class="action login" rel="nofollow" title="Login">Login</a></li>                </ul>
            </div>
        
        <!-- SEARCH TOOLS -->
        <div id="dokuwiki__searchtools">
            <h3 class="a11y"></h3>
            <form action="../../start.html" accept-charset="utf-8" class="search" id="dw__search" method="get" role="search"><div class="no"><input type="hidden" name="do" value="search" /><input type="text" id="qsearch__in" accesskey="f" name="id" class="edit" title="[F]" /><input type="submit" value="Search" class="button" title="Search" /><div id="qsearch__out" class="ajax_qsearch JSpopup"></div></div></form>        </div>

        <!-- SITE TOOLS -->
        <div id="dokuwiki__sitetools">
            <h3 class="a11y">Site Tools</h3>
                            <div class="mobileTools">
                    <li><a href="start.html"  class="action login" rel="nofollow" title="Login">Login</a></li>                </div>
                <ul>
                                    </ul>
                    </div>
    </div>

    <!-- BREADCRUMBS -->
    
    
    <hr class="a11y" />
</div></div><!-- /header -->

        <div class="wrapper group">

            
            <!-- ********** CONTENT ********** -->
            <div id="dokuwiki__content"><div class="pad group">
                <div class="pageId"><span>tutorial:stg:buck:start</span></div>
                <div class="page group">
                                                            <!-- wikipage start -->
                    <!-- TOC START -->
<div id="dw__toc">
<h3 class="toggle">Table of Contents</h3>
<div>

<ul class="toc">
<li class="level1"><div class="li"><a href="#modelling">Modelling</a></div></li>
<li class="level1"><div class="li"><a href="#verification_of_specification">Verification of specification</a></div></li>
<li class="level1"><div class="li"><a href="#synthesis">Synthesis</a></div></li>
<li class="level1"><div class="li"><a href="#circuit_capturing">Circuit capturing</a></div></li>
<li class="level1"><div class="li"><a href="#verification_of_implementation">Verification of implementation</a></div></li>
<li class="level1"><div class="li"><a href="#solutions">Solutions</a></div></li>
</ul>
</div>
</div>
<!-- TOC END -->

<h1 class="sectionedit1" id="synthesis_and_verification_of_buck_control">Synthesis and verification of buck control</h1>
<div class="level1">

<p>
<a href="http://en.wikipedia.org/wiki/Buck converter" class="interwiki iw_wp" title="http://en.wikipedia.org/wiki/Buck converter">Buck converter</a> is a voltage step down and current step up converter. It comprises an analogue buck and its digital control logic as shown in the following diagram. Your task in this tutorial is to formally specify, synthesise and verify the control circuitry of the buck.
</p>

<p>
<img src="schematic-buck.png" class="mediacenter" title="Schematic" alt="Schematic" />
</p>

<p>
The control opens and closes the power regulating PMOS and NMOS transistors of the buck as a reaction to under voltage (UV), over current (OC) and zero crossing (ZC) conditions. These conditions are detected and signalled by a set of specialised sensors implemented as comparators of measured current and voltage levels against some reference values (I_max, V_0, V_ref).
</p>

<p>
The operation of a buck is usually specified in an intuitive, but rather informal way, e.g. by enumerating the possible sequences of detected conditions and describing the intended reaction to these events, as in the following phase diagram.
<img src="pd-buck.png" class="mediacenter" title="Informal specification using phase diagrams" alt="Informal specification using phase diagrams" />
</p>

<p>
This specification reveals an alternation of the UV and OC conditions which are handled by opening and closing PMOS and NMOS transistors of the buck. Detection of the ZC condition after UV does not change this behaviour, however, if ZC is detected before UV then both the PMOS and NMOS transistors remain closed until the UV event. 
</p>

<p>
It is important to note that in order to avoid a short-circuit the PMOS and NMOS transistors of the buck must never be open at the same time.
</p>

</div>

<h2 class="sectionedit2" id="modelling">Modelling</h2>
<div class="level2">

<p>
According to the phase diagram there are three distinctive scenarios to capture:
</p>
<ul>
<li class="level1"><div class="li">
 <strong>no ZC</strong> – UV happens without ZC;
</div></li>
<li class="level1"><div class="li">
 <strong>late ZC</strong> – UV is followed by ZC;
</div></li>
<li class="level1"><div class="li">
 <strong>early ZC</strong> – UV happens after ZC. 
</div></li>
</ul>


<p>
Let us capture one of the scenarios, e.g. when UV happens without ZC, in an STG form (create a new STG work and follow the instructions below).
</p>
<ul>
<li class="level1"><div class="li"> Initially the NMOS transistor is open and the PMOS transistor is closed which should lead to the UV condition:</div>
<ul>
<li class="level3"><div class="li"> Create a place <code>p0</code> and mark it with a token - this denotes the initial state. </div>
</li>
<li class="level3"><div class="li"> Create a rising phase of an input signal and call it <code>uv+</code>.</div>
</li>
<li class="level3"><div class="li"> Connect the place <code>p0</code> to the transition <code>uv+</code>.</div>
</li>
</ul>
</li>
<li class="level1"><div class="li"> When UV is detected the NMOS transistor needs to get closed:</div>
<ul>
<li class="level2"><div class="li"> Create an output transition <code>gn-</code>. </div>
</li>
<li class="level2"><div class="li"> Connect <code>uv+</code> to <code>gn-</code>.</div>
</li>
</ul>
</li>
<li class="level1"><div class="li"> Wait for indication of NMOS transistor being closed:</div>
<ul>
<li class="level2"><div class="li"> Create an input transition <code>gn_ack-</code>.</div>
</li>
<li class="level2"><div class="li"> Connect <code>gn-</code> to <code>gn_ack-</code>,</div>
</li>
</ul>
</li>
<li class="level1"><div class="li"> When the closing of NMOS is confirmed the PMOS transistor can be open to charge the buck:</div>
<ul>
<li class="level2"><div class="li"> Create an output transition <code>gp+</code> and an input transition <code>gp_ack+</code>. </div>
</li>
<li class="level2"><div class="li"> Connect <code>gn_ack-</code> to <code>gp+</code> and <code>gp+</code> to <code>gp_ack+</code>.</div>
</li>
</ul>
</li>
<li class="level1"><div class="li"> Eventually the buck will saturate leading to reset of UV and OC condition:</div>
<ul>
<li class="level2"><div class="li"> Create input transitions <code>uv-</code> and <code>oc+</code>.</div>
</li>
<li class="level2"><div class="li"> Connect <code>gp_ack+</code> to <code>uv-</code> and <code>uv-</code> to <code>oc+</code>.</div>
</li>
</ul>
</li>
<li class="level1"><div class="li"> At this stage the PMOS transistor needs to be closed:</div>
<ul>
<li class="level2"><div class="li"> Create an output transition <code>gp-</code> and an input transition <code>gp_ack-</code>.</div>
</li>
<li class="level2"><div class="li"> Connect <code>oc+</code> to <code>gp-</code> and <code>gp-</code> to <code>gp_ack-</code>.</div>
</li>
</ul>
</li>
<li class="level1"><div class="li"> After closing of the PMOS transistor is confirmed the NMOS transistor gets open:</div>
<ul>
<li class="level2"><div class="li"> Create an output transition <code>gn+</code> and an input transition <code>gn_ack+</code>.</div>
</li>
<li class="level2"><div class="li"> Connect <code>gp_ack-</code> to <code>gn+</code> and <code>gn+</code> to <code>gn_ack+</code>.</div>
</li>
</ul>
</li>
<li class="level1"><div class="li"> This leads to the release of OC and brings us to the initial state:</div>
<ul>
<li class="level2"><div class="li"> Create an input transition <code>oc-</code>.</div>
</li>
<li class="level2"><div class="li"> Connect <code>gn_ack+</code> to <code>oc-</code>.</div>
</li>
<li class="level2"><div class="li"> Connect <code>oc-</code> to the place <code>p0</code>.</div>
</li>
</ul>
</li>
</ul>

<p>
The resultant STG listing the sequence of signal events for this scenario is shown in the following diagram. Save this model as <em>stg-buck-scenario1_no_zc.work</em> file.
</p>

<p>
<img src="stg-buck-scenario1_no_zc.png" class="mediacenter" alt="" />
</p>

<p>
The scenarios for late ZC is formalised in a very similar ways. Both phases of ZC just happen concurrently with closing of NMOS and opening PMOS transistors.
</p>
<ul>
<li class="level1"><div class="li"> Save the no ZC scenario with new name <em>stg-buck-scenario2_late_zc</em>.</div>
</li>
<li class="level1"><div class="li"> Create two input signal transitions <code>zc+</code> and <code>zc-</code>.</div>
</li>
<li class="level1"><div class="li"> Connect <code>uv+</code> to <code>zc+</code>.</div>
</li>
<li class="level1"><div class="li"> Connect <code>zc+</code> to <code>zc-</code>.</div>
</li>
<li class="level1"><div class="li"> Connect <code>zc-</code> to <code>uv-</code>.</div>
</li>
</ul>

<p>
The resultant STG should look similar to the following diagram. Do not forget to save the work!
</p>

<p>
<img src="stg-buck-scenario2_late_zc.png" class="mediacenter" alt="" />
</p>

<p>
The scenario for early arrival of ZC is a bit different. Here the NMOS transistor needs to get closed as soon as ZC is detected, without waiting for UV. However, opening of the PMOS transistor is still delayed till UV condition.
</p>
<ul>
<li class="level1"><div class="li"> Save the late ZC model under new name <em>stg-buck-scenario3_early_zc</em>.</div>
</li>
<li class="level1"><div class="li"> Delete incoming and outgoing arcs of <code>uv+</code> and <code>zc+</code> transitions (just select the arc and press <kbd>Delete</kbd>).</div>
</li>
<li class="level1"><div class="li"> Connect place <code>p0</code> to <code>zc+</code> and <code>zc+</code> to <code>gn-</code>.</div>
</li>
<li class="level1"><div class="li"> Connect <code>zc+</code> to <code>uv+</code> and <code>uv+</code> to <code>gp+</code>.</div>
</li>
<li class="level1"><div class="li"> Connect <code>gp+</code> to <code>zc-</code>.</div>
</li>
<li class="level1"><div class="li"> Rearrange transitions to make the STG look nicer (using the selection tool) and save the work.</div>
</li>
</ul>

<p>
The STG for early ZC scenario should look similar to the following diagram.
</p>

<p>
<img src="stg-buck-scenario3_early_zc.png" class="mediacenter" alt="" />
</p>

<p>
These three behavioural scenarios of the buck operation can be synthesised into independent circuits. However, in order to produce an implementation capable of handling all of the scenarios, these STGs need to be composed into a single specification.
</p>

<p>
One can see that all three STGs have ‘compatible’ initial states, that is all common input and output signals are set to the same values initially. Therefore we can merge the initially marked place in the three STGs and obtain a combined specification for buck control.
</p>
<ul>
<li class="level1"><div class="li">
 Create a new STG work called <em>stg-buck-scenarios_combined</em>.
</div></li>
<li class="level1"><div class="li">
 Insert the STG for no ZC scenario by selecting <em>File→Merge work…</em> menu item and choosing the <em>stg-buck-scenario1_no_zc.work</em> file. After insertion the whole STG is selected - drag-and-drop it aside of the centre as the following steps will insert STGs there.
</div></li>
<li class="level1"><div class="li">
 Similarly insert the STG for early ZC scenario (<em>stg-buck-scenario3_early_zc.work</em> file) and drag it below the no ZC scenario.
</div></li>
<li class="level1"><div class="li">
 Finally insert the STG for late ZC scenario (<em>stg-buck-scenario2_late_zc.work</em> file) and drag it above the previously inserted ones.
</div></li>
<li class="level1"><div class="li">
 Now as you have STGs for all three scenarios in the same work space remove the initial place in two of the scenarios (e.g. in late ZC and early ZC) and reuse the remaining place instead.
</div></li>
</ul>


<p>
The STG combining all three scenarios should look like the following diagram. Do not forget to save the work!
</p>

<p>
<img src="stg-buck-scenarios_combined.png" class="mediacenter" alt="" />
</p>
<div class="wrap_info plugin_wrap">
<h4 id="optional_simplification">Optional simplification</h4>

<p>
Once the initially marked places are merged, one can notice that three transitions <code>oc-</code> leading to it can also be merged because their preceding states are ‘compatible’. This process continues with signal event <code>gn_ack+</code>, and so on, ‘zipping’ the common paths of the STGs together. The simplified STG specification for buck control is the following; save it as <em>stg-buck-simplified</em> work. file.
</p>

<p>
<img src="stg-buck-simplified.png" class="mediacenter" alt="" />
</p>

<p>
Note that this STG is just a cosmetic improvement over the original one and can be safely skipped. This should not impact on the verification of synthesis steps.
</p>
</div>
</div>

<h2 class="sectionedit5" id="verification_of_specification">Verification of specification</h2>
<div class="level2">

<p>
Activate the <strong>simulation tool</strong> <img src="../../../help/editor_tools-simulate.png" class="media" title="[M] Simulate" alt="[M] Simulate" /> and exercise the obtained STG model. Click one of the enabled signal transitions (they are highlighted in orange) to <em>evaluate</em> the STG into the next state. Make sure the simulation traces correspond to those intended by the informal specification of the phase diagram.
</p>

<p>
Before proceeding to the synthesis step verify the specification for signal consistency (i.e. that the rising and falling phases of each signal alternate in all possible execution traces) and deadlocks.The former is verified via <em>Tools→Verification→Check for consistency [MPSat]</em> menu and the later  via <em>Tools→Verification→Check for deadlocks [MPSat]</em> menu. 
</p>

<p>
Another property you need to verify is that PMOS and NMOS transistors are never open simultaneously, i.e. that signals <code>gp</code> and <code>gn</code> are never hight at the same time. This design-specific property can be formulated as a reachability analysis problem using <a href="../../../help/reach.html" class="wikilink1" title="help:reach">Reach language</a>:
</p>
<ul>
<li class="level1"><div class="li">
 Open a specialised MPSat configuration window by selecting <em>Tools→Verification→Custom properties [MPSat]…</em> menu.
</div></li>
<li class="level1"><div class="li">
 In <em>MPSat settings</em> set the <em>Mode</em> into <em>STG reachability analysis</em> and the <em>Solution</em> into <em>Minimise cost function</em>.
</div></li>
<li class="level1"><div class="li">
 Give this this property a meaningful name, e.g. <em>Short circuit check</em> 
</div></li>
<li class="level1"><div class="li">
 Enter a Reach expression that identifies the short-circuit, i.e. both <code>gp</code> and <code>gn</code> signals are high – <code>$S“gp” &amp; $S“gn”</code>. <sup><a href="#fn__1" id="fnt__1" class="fn_top">1)</a></sup>.
</div></li>
<li class="level1"><div class="li">
 Save this property it as a preset for future use, e.g. under <em>short circuit check</em> name.
</div></li>
</ul>


<p>
The whole custom property window should look as follows.
</p>

<p>
<img src="property_check-short_circuit.png" class="mediacenter" alt="" />
</p>

<p>
When you click the <em>Run</em> button the STG will be searched for a state where the Reach expression evaluates to <em>True</em>. If such a state exists then the property is violated. Otherwise, the property is satisfied.
</p>

<p>
If the verified property is violated, then a trace leading to the problematic state is reported. This trace can be simulated to diagnose the problem and correct it at the level of STG specification.
</p>

</div>

<h2 class="sectionedit6" id="synthesis">Synthesis</h2>
<div class="level2">

<p>
The STG specification can now be synthesised into an asynchronous circuit implementation either with Petrify or MPSat backend tools via <em>Tools→Synthesis</em> menu.
</p>

<p>
A complex gate solution obtained with Petrify (via <em>Complex gate synthesis [Petrify]</em> menu) is as follows <span class="wrap_important ">Note that solution is not unique and you may get a slightly different set of equations.</span>
:
</p>
<pre class="code">[gp] = uv gn_ack&#039; + gp_ack oc&#039;; 
[gn] = zc&#039; uv&#039; gp_ack&#039;; </pre>

<p>
Using De Morgan&#039;s low one can derive the following negative gate implementation:
</p>
<pre class="code">[gp] = ((uv&#039; + gn_ack) (gp_ack&#039; + oc))&#039;; 
[gn] = (zc + uv + gp_ack)&#039;; </pre>

<p>
These equations can be mapped into complex gates with the following functions: <code>Z=(A&#039;+B)*(C&#039;+D))</code>&#039; for <code>gp</code> and <code>Z=(A+B+C)</code>&#039; for <code>gn</code>. Let us call the former gate <em>NAO2N2N</em> and the later <em>NR3</em>.
</p>

<p>
Association of the pins is best describe by the following Verilog netlist:
</p>
<pre class="code verilog"><span class="kw1">module</span> control <span class="br0">&#40;</span>oc<span class="sy0">,</span> uv<span class="sy0">,</span> zc<span class="sy0">,</span> gp_ack<span class="sy0">,</span> gn_ack<span class="sy0">,</span> gp<span class="sy0">,</span> gn<span class="br0">&#41;</span><span class="sy0">;</span>
  <span class="kw1">input</span> oc<span class="sy0">,</span> uv<span class="sy0">,</span> zc<span class="sy0">,</span> gp_ack<span class="sy0">,</span> gn_ack<span class="sy0">;</span>
  <span class="kw1">output</span> gp<span class="sy0">,</span> gn<span class="sy0">;</span>
  NAO2N2N inst_gp <span class="br0">&#40;</span>.A<span class="br0">&#40;</span>uv<span class="br0">&#41;</span><span class="sy0">,</span> .B<span class="br0">&#40;</span>gn_ack<span class="br0">&#41;</span><span class="sy0">,</span> .C<span class="br0">&#40;</span>gp_ack<span class="br0">&#41;</span><span class="sy0">,</span> .D<span class="br0">&#40;</span>oc<span class="br0">&#41;</span><span class="sy0">,</span> .Z<span class="br0">&#40;</span>gp<span class="br0">&#41;</span><span class="br0">&#41;</span><span class="sy0">;</span>
  NR3 inst_gn <span class="br0">&#40;</span>.A<span class="br0">&#40;</span>zc<span class="br0">&#41;</span><span class="sy0">,</span> .B<span class="br0">&#40;</span>uv<span class="br0">&#41;</span><span class="sy0">,</span> .C<span class="br0">&#40;</span>gp_ack<span class="br0">&#41;</span><span class="sy0">,</span> .Z<span class="br0">&#40;</span>gn<span class="br0">&#41;</span><span class="br0">&#41;</span><span class="sy0">;</span>
<span class="kw1">endmodule</span></pre>

</div>

<h2 class="sectionedit7" id="circuit_capturing">Circuit capturing</h2>
<div class="level2">

<p>
Create a new Digital Circuit work called <em>circuit-buck-cg</em> and capture the implementation suggested by Petrify in form of a gate-level netlist. <span class="wrap_info ">In the future versions of Workcraft the derivation of a circuit from the synthesis output will be automated, but for now please do it manually.</span>
</p>
<ul>
<li class="level1"><div class="li">
 Create a Digital Circuit work <em>circuit-buck-cg</em>.
</div></li>
<li class="level1"><div class="li">
 Add a functional component with a set function <code>((A&#039; + B) * (C&#039; + D))&#039;</code> <sup><a href="#fn__2" id="fnt__2" class="fn_top">2)</a></sup>. Rename it to <code>inst_gp</code> and change its rendering type to <em>GATE</em>.
</div></li>
<li class="level1"><div class="li">
 Add a functional component with a set function <code>(A + B + C)&#039;</code> <sup><a href="#fn__3" id="fnt__3" class="fn_top">3)</a></sup>. Rename it to <code>inst_gn</code> and change its rendering type to <em>GATE</em>.
</div></li>
<li class="level1"><div class="li">
 Create two output ports <code>gp</code> and <code>gn</code>. 
</div></li>
<li class="level1"><div class="li">
 Connect the output of <code>inst_gp</code> to the <code>gp</code> port and the output of <code>inst_gn</code> gate to the <code>gn</code> port.
</div></li>
<li class="level1"><div class="li">
 Create input ports <code>gn_ack</code>, <code>oc</code>, <code>uv</code>, <code>zc</code> and <code>gp_ack</code>.
</div></li>
<li class="level1"><div class="li">
 Connect the input port to the corresponding pins of the <code>inst_gp</code> and <code>inst_gn</code> gates. Make use of <strong>joint generator</strong> <img src="../../../help/editor_tools-joint.png" class="media" title="[J] Joint" alt="[J] Joint" /> for forking the connections.
</div></li>
</ul>


<p>
The captured circuit should look like this. 
</p>

<p>
<img src="circuit-buck-cg.png" class="mediacenter" alt="" />
</p>

</div>

<h2 class="sectionedit8" id="verification_of_implementation">Verification of implementation</h2>
<div class="level2">

<p>
Activate the <strong>simulation tool</strong> <img src="../../../help/editor_tools-simulate.png" class="media" title="[M] Simulate" alt="[M] Simulate" /> and simulate the captured complex gate implementation of the buck control. Ports, pins and wires are colour-coded: blue means low level and red means high level of the signal. Excited pins and ports are highlighted in orange. 
</p>

<p>
Click an exited pin to toggle its logical value – the circuit will evaluate to the next state where new set of signals will be enabled. The sequence of signal events is recorded in the simulation trace and can be subsequently replayed for analysing the circuit behaviour.
</p>

<p>
Note that the switching of input ports is not restricted. Environment can change them at any time causing unspecified behaviour of the circuit. You can restrict this behaviour by composing the circuit with the specification of its environment. The STG that was used at the synthesis stage is a good candidate for such a specification as it models both the buck control and its environment.
</p>
<ul>
<li class="level1"><div class="li">
 Activate <strong>selection tool</strong> and make sure nothing is selected – the Property editor will shoow the properties of the whole circuit.
</div></li>
<li class="level1"><div class="li">
 Click the <em>Environment <abbr title="Uniform Resource Identifier">URI</abbr></em> property - a file browser will pop up. Locate the <em>stg-buck-scenarios_composed.work</em> file and open it. A path to that file will be copied to the <em>Environment <abbr title="Uniform Resource Identifier">URI</abbr></em> property <sup><a href="#fn__4" id="fnt__4" class="fn_top">4)</a></sup>.
</div></li>
</ul>


<p>
Now all the circuit verification will be made in the context of the environment that behaves according to STG in <em>stg-buck-scenarios_composed.work</em> file. Check the circuit for hazards, deadlocks and verify if it conforms to the environment specification. All these verification steps can be run via <em>Tools→Verification→Check circuit for conformation, deadlocks and hazards (reuse unfolding)</em> menu.
</p>

<p>
Try to alter the circuit and verify if it still conforms to the environment, is deadlock-free and operates without hazards.
</p>

</div>

<h2 class="sectionedit9" id="solutions">Solutions</h2>
<div class="level2">

<p>
Download all the Workcraft models discussed in this tutorial here:
</p>

<p>
<span class="wrap_download "><a href="buck.tar.gz" class="media mediafile mf_gz" title="tutorial:stg:buck:buck.tar.gz (23.2 KB)">Buck control models</a> (23.18 KiB, <acronym title="Modified: 2014-11-14 17:06.37">47m ago</acronym>)</span>
</p>

</div>
<div class="footnotes">
<div class="fn"><sup><a href="#fnt__1" id="fn__1" class="fn_bot">1)</a></sup> 
Here <code>$S</code> means the value of a signal, <code>“gp”</code> and <code>“gn”</code> are the names of the signals and <code>&amp;</code> is a Boolean AND</div>
<div class="fn"><sup><a href="#fnt__2" id="fn__2" class="fn_bot">2)</a></sup> 
, <sup><a href="#fnt__3" id="fn__3" class="fn_bot">3)</a></sup> 
Notice the use of <code>&#039;</code> symbol for negation.</div>
<div class="fn"><sup><a href="#fnt__4" id="fn__4" class="fn_bot">4)</a></sup> 
If the file does not exist, then its name is shown in red.</div>
</div>

                    <!-- wikipage stop -->
                                    </div>

                                            </div></div><!-- /content -->

            <hr class="a11y" />

            <!-- PAGE ACTIONS -->
            <div id="dokuwiki__pagetools">
                        </div>
        </div><!-- /wrapper -->

        
<!-- ********** FOOTER ********** -->
<div id="dokuwiki__footer"><div class="pad">
    
    <div class="buttons">
                <a href="http://www.dokuwiki.org/donate" title="Donate" ><img
            src="../../lib/tpl/dokuwiki-light-export/images/button-donate.gif" width="80" height="15" alt="Donate" /></a>
        <a href="http://www.php.net" title="Powered by PHP" ><img
            src="../../lib/tpl/dokuwiki-light-export/images/button-php.gif" width="80" height="15" alt="Powered by PHP" /></a>
        <a href="http://validator.w3.org/check/referer" title="Valid HTML5" ><img
            src="../../lib/tpl/dokuwiki-light-export/images/button-html5.png" width="80" height="15" alt="Valid HTML5" /></a>
        <a href="http://jigsaw.w3.org/css-validator/check/referer?profile=css3" title="Valid CSS" ><img
            src="../../lib/tpl/dokuwiki-light-export/images/button-css.png" width="80" height="15" alt="Valid CSS" /></a>
        <a href="http://dokuwiki.org/" title="Driven by DokuWiki" ><img
            src="../../lib/tpl/dokuwiki-light-export/images/button-dw.png" width="80" height="15" alt="Driven by DokuWiki" /></a>
    </div>

    <div class="userInfo">
            </div>
</div></div><!-- /footer -->

    </div></div><!-- /site -->

    <div class="no"><img  width="2" height="1" alt="" /></div>
    <div id="screen__mode" class="no"></div>    <!--[if ( lte IE 7 | IE 8 ) ]></div><![endif]-->
</body>
</html>

